module Number

open Bus
open Time
open Map
open Monitor

sig Number {

	route: Route -> Time,
	buses: Bus -> Time,
	nextBus: Bus ->Time
}

fact thereIsJustOneNextBus{
	all n:Number, t:Time| some b:Bus | b in n.buses.t and n.nextBus.t = b
}

fact numbersHaveDiffBuses{
	all disj n1,n2:Number | all t:Time | diffBuses[n1,n2,t]
}

pred diffBuses[n1 : Number, n2:Number, t : Time] {
	n1.buses.t !in n2.buses.t
}

fact numbersHaveDiffRoutes{
	all disj n1,n2:Number | all t:Time | diffRoutes[n1, n2, t]
}

pred diffRoutes[n1 : Number, n2 : Number, t : Time] {
	(n1.route).t != (n2.route).t
}

fact numberHaveRoute{
	all n:Number | all t:Time | one r:Route | n.route.t = r
}
